Built with Alectryon, running Coq+SerAPI v8.13.0+0.13.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
(******************************************************************************)(* *)(* Generalised Hanoi Problem *)(* *)(******************************************************************************)(* *)(* We consider a generalisation of Hanoi problem : *)(* a parameter n : the number of pegs *)(* a parameter r : r p1 p2 tells that a disk can go from p1 -> p2 *)(* *)(* peg n == type for pegs (there are n pegs) *)(* disk k == type for disks (there are k disk) *)(* configuration k n == type for hanoi configuration with *)(* k disks and n pegs *)(* ldisk == the largest disk *)(* sdisk == the smallest disk *)(* d1 \larger d2 == disk d1 is larger than disk d2 *)(* c d == the peg on which the disk d in the configuration c *)(* `c[p] == a configuration with n disk where all the disks *)(* `p[p1, p2] == pick a peg (if possible) that is diffenent from p1 *)(* and p2 *)(* are on peg p *)(* on_top d c == the disk c is on top of its peg on the *)(* configuration c *)(* rrel == a regular relation between pegs, rrel p1 p2 is *)(* true iff peg p1 is different from peg p2 *)(* lrel == a linear relation between pegs, lrel p1 p2 is *)(* true iff peg p1 is next to peg p2 *)(* srel == a star relation between pegs, srel p1 p2 is *)(* true iff p1 != p2 and p1 or p2 is the 0 peg *)(* move r c1 c2 == checks if going from configuration c1 *)(* to configuration c2 is a move compatible with *)(* relation r (a relation over pegs) *)(* cdisjoint c1 c2 == configurations c1 and c2 are on different pegs *)(* cmerge c1 c2 == merge a configuration c1 with m disk and a *)(* a configuration with n disks to get a configuration*)(* with m + n disk *)(* crshift c == right shift a configuration c with m + n disks, to *)(* get a configuration with n disks taking the disks *)(* larger than m *)(* clshift c == right shift a configuration c with m + n disks, to *)(* get a configuration with n disks taking the disks *)(* smaller than m *)(* ↑[c]_ p == lift a configuration by adding a largest disk on *)(* peg p. This lifting is done from the largest one *)(* so to accomodate the usual induction *)(* ↓[c] == unlift a configuration by removing the largest *)(* disk *)(* plift i p == lift a configuration by adding a new empty peg i *)(* *)(******************************************************************************)
Notation"[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation"_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation"_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation"_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation"_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
From hanoi Require Import extra gdist.Set Implicit Arguments.Unset Strict Implicit.Unset Printing Implicit Defensive.SectionGHanoi.Variableq : nat.(******************************************************************************)(* The pegs are the elements of 'I_q *)(******************************************************************************)Definitionpeg := 'I_q.Variabler : rel peg.HypothesisirH : irreflexive r.HypothesissymH : symmetric r.SectionDisk.(******************************************************************************)(* The disks are represented with the element of 'I_n with *)(* the idea that disk d1 is larger than disk d2 is d2 <= d1. *)(******************************************************************************)Variablen : nat.Definitiondisk := 'I_n.Definitionmk_diskm (H : m < n) : disk := Ordinal H.(******************************************************************************)(* Given a configuration c, the disks on the peg p can be reconstructed by *)(* the list in decreasing order of the disk d such that c d = p *)(******************************************************************************)Definitionconfiguration := {ffun disk -> peg}.(* A perfect configuration is one where all the pegs are on a single peg p *)Definitionperfectp : configuration := [ffun d => p].EndDisk.Arguments perfect [n].Local Notation"`c[ p ] " := (perfect p)
(format"`c[ p ]", at level5).(* The smallest disk *)Definitionsdisk {n} : disk n.+1 := ord0.
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
d:disk 1
d = sdisk
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
d:disk 1
d = sdisk
byapply/val_eqP; case: d => [] [].Qed.
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
c1, c2:configuration 1
(c1 == c2) = (c1 sdisk == c2 sdisk)
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
c1, c2:configuration 1
(c1 == c2) = (c1 sdisk == c2 sdisk)
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
c1, c2:configuration 1
c1 sdisk = c2 sdisk -> c1 = c2
bymove=> H; apply/ffunP=> i; rewrite [i]disk1_all.Qed.(* The largest disk *)Definitionldisk {n} : disk n.+1 := ord_max.(******************************************************************************)(* The disk d is on top of peg (c d) *)(******************************************************************************)Definitionon_topn (d : disk n) (c : configuration n) :=
[foralld1 : disk n, (c d == c d1) ==> (d <= d1)].
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
n:nat
d:disk n
c:configuration n
reflect
(foralld1 : ordinal_finType n,
c d = c d1 -> d <= d1) (on_top d c)
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
n:nat
d:disk n
c:configuration n
reflect
(foralld1 : ordinal_finType n,
c d = c d1 -> d <= d1) (on_top d c)
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
n:nat
d:disk n
c:configuration n
H:forallx : ordinal_finType n,
(c d == c x) ==> (d <= x)
d1:ordinal_finType n
cdEcd1:c d = c d1
d <= d1
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
n:nat
d:disk n
c:configuration n
H:foralld1 : ordinal_finType n,
c d = c d1 -> d <= d1
d1:ordinal_finType n
(c d == c d1) ==> (d <= d1)
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
n:nat
d:disk n
c:configuration n
H:foralld1 : ordinal_finType n,
c d = c d1 -> d <= d1
d1:ordinal_finType n
(c d == c d1) ==> (d <= d1)
byapply/implyP=> /eqP /H.Qed.(******************************************************************************)(* A move is a relation between two configurations c1 c2: *)(* there must exist a disk d1, that is the only one that has changed of *)(* peg (c1 d1 != c2 d1) that is on top of c1 and c2 *)(******************************************************************************)Definitionmove {n} : rel (configuration n) :=
[rel c1 c2 | [existsd1 : disk n,
[&& r ((c1 : configuration n) d1) (c2 d1),
[foralld2, (d1 != d2) ==> (c1 d2 == c2 d2)],
on_top d1 c1 &
on_top d1 c2]]].
bycase/eqP: H5; apply: H2; rewrite eq_sym.Qed.(* this holds if r is symmetric *)
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
n:nat
c1, c2:configuration n
move c1 c2 = move c2 c1
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
n:nat
c1, c2:configuration n
move c1 c2 = move c2 c1
byapply/moveP/moveP=> [] [d [H1 H2 H3 H4]];
existsd; split; rewrite1?symH1?eq_sym // => e dDe; apply/sym_equal/H2.Qed.(* In a move, the disk that moves accomodates r *)
move c1 c2 -> c1 d != c2 d -> d1 <= d -> c2 d1 != c1 d
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
n:nat
d, d1:disk n
c1, c2:configuration n
move c1 c2 -> c1 d != c2 d -> d1 <= d -> c2 d1 != c1 d
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
n:nat
d, d1:disk n
c1, c2:configuration n
c1Mc2:move c1 c2
c1Dc2:c1 d != c2 d
c2 d != c1 d
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
n:nat
d, d1:disk n
c1, c2:configuration n
c1Mc2:move c1 c2
c1Dc2:c1 d != c2 d
dLd1:d1 < d
c2 d1 != c1 d
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
n:nat
d, d1:disk n
c1, c2:configuration n
c1Mc2:move c1 c2
c1Dc2:c1 d != c2 d
dLd1:d1 < d
c2 d1 != c1 d
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
n:nat
d, d1:disk n
c1, c2:configuration n
c1Mc2:move c1 c2
c1Dc2:c1 d != c2 d
dLd1:d1 < d
d1 != d
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
n:nat
d, d1:disk n
c1, c2:configuration n
c1Mc2:move c1 c2
c1Dc2:c1 d != c2 d
dLd1:d1 < d
~~ (d <= d1) -> c1 d != c1 d1
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
n:nat
d, d1:disk n
c1, c2:configuration n
c1Mc2:move c1 c2
c1Dc2:c1 d != c2 d
dLd1:d1 < d
~~ (d <= d1) -> c1 d != c1 d1
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
n:nat
d, d1:disk n
c1, c2:configuration n
c1Mc2:move c1 c2
c1Dc2:c1 d != c2 d
dLd1:d1 < d
c1 d = c1 d1 -> d <= d1
have /on_topP := move_on_topl c1Mc2 c1Dc2; apply.Qed.(* configuration on different pegs *)Definitioncdisjointmn (c1 : configuration m) (c2 : configuration n) :=
[foralli, [forallj, c1 i != c2 j]].
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration m
c2:configuration n
reflect
(forall (i : ordinal_finType m)
(j : ordinal_finType n), c1 i != c2 j)
(cdisjoint c1 c2)
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration m
c2:configuration n
reflect
(forall (i : ordinal_finType m)
(j : ordinal_finType n), c1 i != c2 j)
(cdisjoint c1 c2)
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration m
c2:configuration n
H:forallx : ordinal_finType m,
[forallj, c1 x != c2 j]
i:ordinal_finType m
j:ordinal_finType n
c1 i != c2 j
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration m
c2:configuration n
H:forall (i : ordinal_finType m)
(j : ordinal_finType n),
c1 i != c2 j
i:ordinal_finType m
[forallj, c1 i != c2 j]
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration m
c2:configuration n
H:forall (i : ordinal_finType m)
(j : ordinal_finType n),
c1 i != c2 j
i:ordinal_finType m
[forallj, c1 i != c2 j]
byapply/forallP=> j; apply: H.Qed.(* merging two configurations : c1 for the small disks, c2 for the big ones *)Definitioncmergemn (c1 : configuration m) (c2 : configuration n) :=
[ffun i => match tsplit i with inl j => c1 j | inr j => c2 j end].(* right shifting a configuration : taking the disks smaller than n *)Definitioncrshiftmn (c : configuration (m + n)) : configuration n :=
[ffun i => c (trshift m i)].(* left shifting a configuration : taking the disks larger than n *)Definitionclshiftmn (c : configuration (m + n)) : configuration m :=
[ffun i => c (tlshift n i)].(* Sanity check *)
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c:configuration (m + n)
cmerge (clshift c) (crshift c) = c
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c:configuration (m + n)
cmerge (clshift c) (crshift c) = c
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c:configuration (m + n)
i:ordinal_finType (m + n)
match tsplit i with
| inl j => clshift c j
| inr j => crshift c j
end = c i
byapply/val_eqP/eqP => /=.Qed.Fixpointrm_rep (A : eqType) (a : A) (s : seq A) :=
if s is b :: s1 thenif a == b then rm_rep b s1 else b :: rm_rep b s1
else [::].
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:eqType
a:A
s:seq A
subseq (rm_rep a s) s
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:eqType
a:A
s:seq A
subseq (rm_rep a s) s
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:eqType
b:A
s:seq A
IH:foralla : A, subseq (rm_rep a s) s
a:A
subseq (rm_rep a (b :: s)) (b :: s)
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:eqType
b:A
s:seq A
IH:foralla : A, subseq (rm_rep a s) s
a:A
subseq (rm_rep b s) (b :: s)
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:eqType
b:A
s:seq A
IH:foralla : A, subseq (rm_rep a s) s
a:A
subseq (b :: rm_rep b s) (b :: s)
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:eqType
b:A
s:seq A
IH:foralla : A, subseq (rm_rep a s) s
a:A
subseq (b :: rm_rep b s) (b :: s)
byrewrite /= eqxx IH.Qed.
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:eqType
a:A
s:seq A
{subset rm_rep a s <= s}
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:eqType
a:A
s:seq A
{subset rm_rep a s <= s}
byapply/mem_subseq/subseq_rm_rep.Qed.
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:eqType
a:A
s:seq A
size (rm_rep a s) <= size s
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:eqType
a:A
s:seq A
size (rm_rep a s) <= size s
byapply/size_subseq/subseq_rm_rep.Qed.
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:eqType
a, b:A
s:seq A
size (rm_rep b s) <= size (rm_rep a (b :: s))
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:eqType
a, b:A
s:seq A
size (rm_rep b s) <= size (rm_rep a (b :: s))
byrewrite /=; case: (_ == _) => //=.Qed.
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:finType
a:A
s1:{set A}
s2:seq A
{subset s1 <= s2} ->
a \notin s1 -> #|s1| <= size (rm_rep a s2)
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:finType
a:A
s1:{set A}
s2:seq A
{subset s1 <= s2} ->
a \notin s1 -> #|s1| <= size (rm_rep a s2)
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:finType
s1:{set A}
a:A
aS:{subset s1 <= [::]}
#|s1| <= 0
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:finType
b:A
s2:seq A
IH:forall (s1 : {set A}) (a : A),
{subset s1 <= s2} ->
a \notin s1 -> #|s1| <= size (rm_rep a s2)
s1:{set A}
a:A
s1S:{subset s1 <= b :: s2}
aNIs1:a \notin s1
#|s1| <=
size
(if a == b then rm_rep b s2 else b :: rm_rep b s2)
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:finType
s1:{set A}
a:A
aS:{subset s1 <= [::]}
i:A
(i \in s1) = (i \in set0)
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:finType
b:A
s2:seq A
IH:forall (s1 : {set A}) (a : A),
{subset s1 <= s2} ->
a \notin s1 -> #|s1| <= size (rm_rep a s2)
s1:{set A}
a:A
s1S:{subset s1 <= b :: s2}
aNIs1:a \notin s1
#|s1| <=
size
(if a == b then rm_rep b s2 else b :: rm_rep b s2)
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:finType
b:A
s2:seq A
IH:forall (s1 : {set A}) (a : A),
{subset s1 <= s2} ->
a \notin s1 -> #|s1| <= size (rm_rep a s2)
s1:{set A}
a:A
s1S:{subset s1 <= b :: s2}
aNIs1:a \notin s1
#|s1| <=
size
(if a == b then rm_rep b s2 else b :: rm_rep b s2)
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:finType
b:A
s2:seq A
IH:forall (s1 : {set A}) (a : A),
{subset s1 <= s2} ->
a \notin s1 -> #|s1| <= size (rm_rep a s2)
s1:{set A}
a:A
s1S:{subset s1 <= b :: s2}
aNIs1:a \notin s1
aEb:a = b
#|s1| <= size (rm_rep b s2)
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:finType
b:A
s2:seq A
IH:forall (s1 : {set A}) (a : A),
{subset s1 <= s2} ->
a \notin s1 -> #|s1| <= size (rm_rep a s2)
s1:{set A}
a:A
s1S:{subset s1 <= b :: s2}
aNIs1:a \notin s1
aDb:a <> b
#|s1| <= size (b :: rm_rep b s2)
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:finType
b:A
s2:seq A
s1:{set A}
a:A
s1S:{subset s1 <= b :: s2}
aNIs1:a \notin s1
aEb:a = b
{subset s1 <= s2}
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:finType
b:A
s2:seq A
IH:forall (s1 : {set A}) (a : A),
{subset s1 <= s2} ->
a \notin s1 -> #|s1| <= size (rm_rep a s2)
s1:{set A}
a:A
s1S:{subset s1 <= b :: s2}
aNIs1:a \notin s1
aDb:a <> b
#|s1| <= size (b :: rm_rep b s2)
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:finType
b:A
s2:seq A
s1:{set A}
a:A
s1S:{subset s1 <= b :: s2}
aNIs1:a \notin s1
aEb:a = b
i:A
is1:i \in s1
(i == b) || (i \in s2) -> i \in s1 -> i \in s2
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:finType
b:A
s2:seq A
IH:forall (s1 : {set A}) (a : A),
{subset s1 <= s2} ->
a \notin s1 -> #|s1| <= size (rm_rep a s2)
s1:{set A}
a:A
s1S:{subset s1 <= b :: s2}
aNIs1:a \notin s1
aDb:a <> b
#|s1| <= size (b :: rm_rep b s2)
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:finType
b:A
s2:seq A
IH:forall (s1 : {set A}) (a : A),
{subset s1 <= s2} ->
a \notin s1 -> #|s1| <= size (rm_rep a s2)
s1:{set A}
a:A
s1S:{subset s1 <= b :: s2}
aNIs1:a \notin s1
aDb:a <> b
#|s1| <= size (b :: rm_rep b s2)
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:finType
b:A
s2:seq A
IH:forall (s1 : {set A}) (a : A),
{subset s1 <= s2} ->
a \notin s1 -> #|s1| <= size (rm_rep a s2)
s1:{set A}
a:A
s1S:{subset s1 <= b :: s2}
aNIs1:a \notin s1
aDb:a <> b
bNIs1:b \notin s1
#|s1| <= (size (rm_rep b s2)).+1
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:finType
b:A
s2:seq A
IH:forall (s1 : {set A}) (a : A),
{subset s1 <= s2} ->
a \notin s1 -> #|s1| <= size (rm_rep a s2)
s1:{set A}
a:A
s1S:{subset s1 <= b :: s2}
aNIs1:a \notin s1
aDb:a <> b
bIs1:b \in s1
#|s1| <= (size (rm_rep b s2)).+1
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:finType
b:A
s2:seq A
IH:forall (s1 : {set A}) (a : A),
{subset s1 <= s2} ->
a \notin s1 -> #|s1| <= size (rm_rep a s2)
s1:{set A}
a:A
s1S:{subset s1 <= b :: s2}
aNIs1:a \notin s1
aDb:a <> b
bNIs1:b \notin s1
{subset s1 <= s2}
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:finType
b:A
s2:seq A
IH:forall (s1 : {set A}) (a : A),
{subset s1 <= s2} ->
a \notin s1 -> #|s1| <= size (rm_rep a s2)
s1:{set A}
a:A
s1S:{subset s1 <= b :: s2}
aNIs1:a \notin s1
aDb:a <> b
bIs1:b \in s1
#|s1| <= (size (rm_rep b s2)).+1
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:finType
b:A
s2:seq A
IH:forall (s1 : {set A}) (a : A),
{subset s1 <= s2} ->
a \notin s1 -> #|s1| <= size (rm_rep a s2)
s1:{set A}
a:A
s1S:{subset s1 <= b :: s2}
aNIs1:a \notin s1
aDb:a <> b
bNIs1:b \notin s1
i:A
is1:i \in s1
(i == b) || (i \in s2) -> i \in s1 -> i \in s2
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:finType
b:A
s2:seq A
IH:forall (s1 : {set A}) (a : A),
{subset s1 <= s2} ->
a \notin s1 -> #|s1| <= size (rm_rep a s2)
s1:{set A}
a:A
s1S:{subset s1 <= b :: s2}
aNIs1:a \notin s1
aDb:a <> b
bIs1:b \in s1
#|s1| <= (size (rm_rep b s2)).+1
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:finType
b:A
s2:seq A
IH:forall (s1 : {set A}) (a : A),
{subset s1 <= s2} ->
a \notin s1 -> #|s1| <= size (rm_rep a s2)
s1:{set A}
a:A
s1S:{subset s1 <= b :: s2}
aNIs1:a \notin s1
aDb:a <> b
bIs1:b \in s1
#|s1| <= (size (rm_rep b s2)).+1
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:finType
b:A
s2:seq A
IH:forall (s1 : {set A}) (a : A),
{subset s1 <= s2} ->
a \notin s1 -> #|s1| <= size (rm_rep a s2)
s1:{set A}
a:A
s1S:{subset s1 <= b :: s2}
aNIs1:a \notin s1
aDb:a <> b
bIs1:b \in s1
#|s1 :\ b| <= size (rm_rep b s2)
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:finType
b:A
s2:seq A
s1:{set A}
a:A
s1S:{subset s1 <= b :: s2}
aNIs1:a \notin s1
aDb:a <> b
bIs1:b \in s1
i:A
i \in s1 :\ b -> i \in s2
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:finType
b:A
s2:seq A
s1:{set A}
a:A
s1S:{subset s1 <= b :: s2}
aNIs1:a \notin s1
aDb:a <> b
bIs1:b \in s1
b \notin s1 :\ b
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:finType
b:A
s2:seq A
s1:{set A}
a:A
s1S:{subset s1 <= b :: s2}
aNIs1:a \notin s1
aDb:a <> b
bIs1:b \in s1
b \notin s1 :\ b
byrewrite !inE eqxx.Qed.
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:eqType
a:A
s:seq A
last a (rm_rep a s) = last a s
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:eqType
a:A
s:seq A
last a (rm_rep a s) = last a s
byelim: s a => //= b l IH a; case: (_ =P _) => /= [->|_]; apply: IH.Qed.
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:eqType
a:A
s1, s2:seq A
rm_rep a (s1 ++ s2) =
rm_rep a s1 ++ rm_rep (last a s1) s2
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:eqType
a:A
s1, s2:seq A
rm_rep a (s1 ++ s2) =
rm_rep a s1 ++ rm_rep (last a s1) s2
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:eqType
b:A
s1:seq A
IH:forall (s2 : seq A) (a : A),
rm_rep a (s1 ++ s2) =
rm_rep a s1 ++ rm_rep (last a s1) s2
s2:seq A
a:A
(if a == b
then rm_rep b (s1 ++ s2)
else b :: rm_rep b (s1 ++ s2)) =
(if a == b then rm_rep b s1 else b :: rm_rep b s1) ++
rm_rep (last b s1) s2
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:eqType
b:A
s1:seq A
IH:forall (s2 : seq A) (a : A),
rm_rep a (s1 ++ s2) =
rm_rep a s1 ++ rm_rep (last a s1) s2
s2:seq A
a:A
aDb:a <> b
b :: rm_rep b (s1 ++ s2) =
b :: rm_rep b s1 ++ rm_rep (last b s1) s2
bycongr (_ :: _); apply: IH.Qed.
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:eqType
a, b:A
s:seq_predType A
b != a -> b \in s -> b \in rm_rep a s
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:eqType
a, b:A
s:seq_predType A
b != a -> b \in s -> b \in rm_rep a s
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:eqType
b, c:A
s:seq A
IH:foralla : A,
b != a -> b \in s -> b \in rm_rep a s
a:A
bDa:b != a
(b == c) || (b \in s) ->
b \in (if a == c then rm_rep c s else c :: rm_rep c s)
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:eqType
b, c:A
s:seq A
IH:foralla : A,
b != a -> b \in s -> b \in rm_rep a s
a:A
bDa:b != a
b \in (if a == b then rm_rep b s else b :: rm_rep b s)
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:eqType
b, c:A
s:seq A
IH:foralla : A,
b != a -> b \in s -> b \in rm_rep a s
a:A
bDa:b != a
bDc:b != c
bIs:b \in s
b \in (if a == c then rm_rep c s else c :: rm_rep c s)
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
A:eqType
b, c:A
s:seq A
IH:foralla : A,
b != a -> b \in s -> b \in rm_rep a s
a:A
bDa:b != a
bDc:b != c
bIs:b \in s
b \in (if a == c then rm_rep c s else c :: rm_rep c s)
byhave := IH _ bDc bIs; case: (_ == _); rewrite // inE orbC => ->.Qed.
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c:configuration (m + n)
cs:seq (configuration (m + n))
path move c cs ->
path move (clshift c)
(rm_rep (clshift c) [seq clshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c:configuration (m + n)
cs:seq (configuration (m + n))
path move c cs ->
path move (clshift c)
(rm_rep (clshift c) [seq clshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
path move (clshift c)
(rm_rep (clshift c) [seq clshift i | i <- cs])
c:configuration (m + n)
cMc1:move c c1
c1Pcs:path move c1 cs
path move (clshift c)
(if clshift c == clshift c1
then rm_rep (clshift c1) [seq clshift i | i <- cs]
else
clshift c1
:: rm_rep (clshift c1) [seq clshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
path move (clshift c)
(rm_rep (clshift c) [seq clshift i | i <- cs])
c:configuration (m + n)
cMc1:move c c1
c1Pcs:path move c1 cs
cDc1:clshift c != clshift c1
move (clshift c) (clshift c1) &&
path move (clshift c1)
(rm_rep (clshift c1) [seq clshift i | i <- cs])
byrewrite move_clshift //=; apply: IH.Qed.
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c:configuration (m + n)
cs:seq (configuration (m + n))
path move c cs ->
path move (crshift c)
(rm_rep (crshift c) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c:configuration (m + n)
cs:seq (configuration (m + n))
path move c cs ->
path move (crshift c)
(rm_rep (crshift c) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
path move (crshift c)
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
cMc1:move c c1
c1Pcs:path move c1 cs
path move (crshift c)
(if crshift c == crshift c1
then rm_rep (crshift c1) [seq crshift i | i <- cs]
else
crshift c1
:: rm_rep (crshift c1) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
path move (crshift c)
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
cMc1:move c c1
c1Pcs:path move c1 cs
cDc1:crshift c != crshift c1
move (crshift c) (crshift c1) &&
path move (crshift c1)
(rm_rep (crshift c1) [seq crshift i | i <- cs])
byrewrite move_crshift //=; apply: IH.Qed.
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c:configuration (m + n)
cs:seq (configuration (m + n))
path move c cs ->
size cs =
size (rm_rep (clshift c) [seq clshift i | i <- cs]) +
size (rm_rep (crshift c) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c:configuration (m + n)
cs:seq (configuration (m + n))
path move c cs ->
size cs =
size (rm_rep (clshift c) [seq clshift i | i <- cs]) +
size (rm_rep (crshift c) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
(size cs).+1 =
size
(if clshift c == clshift c1
then rm_rep (clshift c1) [seq clshift i | i <- cs]
else
clshift c1
:: rm_rep (clshift c1) [seq clshift i | i <- cs]) +
size
(if crshift c == crshift c1
then rm_rep (crshift c1) [seq crshift i | i <- cs]
else
crshift c1
:: rm_rep (crshift c1) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
j:'I_n
dE:d = j
(size cs).+1 =
size
(if clshift c == clshift c1
then rm_rep (clshift c1) [seq clshift i | i <- cs]
else
clshift c1
:: rm_rep (clshift c1) [seq clshift i | i <- cs]) +
size
(if crshift c == crshift c1
then rm_rep (crshift c1) [seq crshift i | i <- cs]
else
crshift c1
:: rm_rep (crshift c1) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
k:'I_m
dE:d = k + n
(size cs).+1 =
size
(if clshift c == clshift c1
then rm_rep (clshift c1) [seq clshift i | i <- cs]
else
clshift c1
:: rm_rep (clshift c1) [seq clshift i | i <- cs]) +
size
(if crshift c == crshift c1
then rm_rep (crshift c1) [seq crshift i | i <- cs]
else
crshift c1
:: rm_rep (crshift c1) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
j:'I_n
dE:d = j
clshift c == clshift c1
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
j:'I_n
dE:d = j
(size cs).+1 =
size (rm_rep (clshift c1) [seq clshift i | i <- cs]) +
size
(if crshift c == crshift c1
then rm_rep (crshift c1) [seq crshift i | i <- cs]
else
crshift c1
:: rm_rep (crshift c1) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
k:'I_m
dE:d = k + n
(size cs).+1 =
size
(if clshift c == clshift c1
then rm_rep (clshift c1) [seq clshift i | i <- cs]
else
clshift c1
:: rm_rep (clshift c1) [seq clshift i | i <- cs]) +
size
(if crshift c == crshift c1
then rm_rep (crshift c1) [seq crshift i | i <- cs]
else
crshift c1
:: rm_rep (crshift c1) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
j:'I_n
dE:d = j
i:ordinal_finType m
c (tlshift n i) = c1 (tlshift n i)
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
j:'I_n
dE:d = j
(size cs).+1 =
size (rm_rep (clshift c1) [seq clshift i | i <- cs]) +
size
(if crshift c == crshift c1
then rm_rep (crshift c1) [seq crshift i | i <- cs]
else
crshift c1
:: rm_rep (crshift c1) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
k:'I_m
dE:d = k + n
(size cs).+1 =
size
(if clshift c == clshift c1
then rm_rep (clshift c1) [seq clshift i | i <- cs]
else
clshift c1
:: rm_rep (clshift c1) [seq clshift i | i <- cs]) +
size
(if crshift c == crshift c1
then rm_rep (crshift c1) [seq crshift i | i <- cs]
else
crshift c1
:: rm_rep (crshift c1) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
j:'I_n
dE:d = j
i:ordinal_finType m
d == i + n -> False
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
j:'I_n
dE:d = j
(size cs).+1 =
size (rm_rep (clshift c1) [seq clshift i | i <- cs]) +
size
(if crshift c == crshift c1
then rm_rep (crshift c1) [seq crshift i | i <- cs]
else
crshift c1
:: rm_rep (crshift c1) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
k:'I_m
dE:d = k + n
(size cs).+1 =
size
(if clshift c == clshift c1
then rm_rep (clshift c1) [seq clshift i | i <- cs]
else
clshift c1
:: rm_rep (clshift c1) [seq clshift i | i <- cs]) +
size
(if crshift c == crshift c1
then rm_rep (crshift c1) [seq crshift i | i <- cs]
else
crshift c1
:: rm_rep (crshift c1) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
j:'I_n
dE:d = j
(size cs).+1 =
size (rm_rep (clshift c1) [seq clshift i | i <- cs]) +
size
(if crshift c == crshift c1
then rm_rep (crshift c1) [seq crshift i | i <- cs]
else
crshift c1
:: rm_rep (crshift c1) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
k:'I_m
dE:d = k + n
(size cs).+1 =
size
(if clshift c == clshift c1
then rm_rep (clshift c1) [seq clshift i | i <- cs]
else
clshift c1
:: rm_rep (clshift c1) [seq clshift i | i <- cs]) +
size
(if crshift c == crshift c1
then rm_rep (crshift c1) [seq crshift i | i <- cs]
else
crshift c1
:: rm_rep (crshift c1) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
j:'I_n
dE:d = j
crshift c != crshift c1
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
j:'I_n
dE:d = j
(size cs).+1 =
size (rm_rep (clshift c1) [seq clshift i | i <- cs]) +
(size (rm_rep (crshift c1) [seq crshift i | i <- cs])).+1
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
k:'I_m
dE:d = k + n
(size cs).+1 =
size
(if clshift c == clshift c1
then rm_rep (clshift c1) [seq clshift i | i <- cs]
else
clshift c1
:: rm_rep (clshift c1) [seq clshift i | i <- cs]) +
size
(if crshift c == crshift c1
then rm_rep (crshift c1) [seq crshift i | i <- cs]
else
crshift c1
:: rm_rep (crshift c1) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
j:'I_n
dE:d = j
cE:c (trshift m j) = c1 (trshift m j)
False
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
j:'I_n
dE:d = j
(size cs).+1 =
size (rm_rep (clshift c1) [seq clshift i | i <- cs]) +
(size (rm_rep (crshift c1) [seq crshift i | i <- cs])).+1
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
k:'I_m
dE:d = k + n
(size cs).+1 =
size
(if clshift c == clshift c1
then rm_rep (clshift c1) [seq clshift i | i <- cs]
else
clshift c1
:: rm_rep (clshift c1) [seq clshift i | i <- cs]) +
size
(if crshift c == crshift c1
then rm_rep (crshift c1) [seq crshift i | i <- cs]
else
crshift c1
:: rm_rep (crshift c1) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
j:'I_n
dE:d = j
cE:c (trshift m j) = c1 (trshift m j)
c d = c1 d
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
j:'I_n
dE:d = j
(size cs).+1 =
size (rm_rep (clshift c1) [seq clshift i | i <- cs]) +
(size (rm_rep (crshift c1) [seq crshift i | i <- cs])).+1
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
k:'I_m
dE:d = k + n
(size cs).+1 =
size
(if clshift c == clshift c1
then rm_rep (clshift c1) [seq clshift i | i <- cs]
else
clshift c1
:: rm_rep (clshift c1) [seq clshift i | i <- cs]) +
size
(if crshift c == crshift c1
then rm_rep (crshift c1) [seq crshift i | i <- cs]
else
crshift c1
:: rm_rep (crshift c1) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
j:'I_n
dE:d = j
(size cs).+1 =
size (rm_rep (clshift c1) [seq clshift i | i <- cs]) +
(size (rm_rep (crshift c1) [seq crshift i | i <- cs])).+1
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
k:'I_m
dE:d = k + n
(size cs).+1 =
size
(if clshift c == clshift c1
then rm_rep (clshift c1) [seq clshift i | i <- cs]
else
clshift c1
:: rm_rep (clshift c1) [seq clshift i | i <- cs]) +
size
(if crshift c == crshift c1
then rm_rep (crshift c1) [seq crshift i | i <- cs]
else
crshift c1
:: rm_rep (crshift c1) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
j:'I_n
dE:d = j
size cs =
size (rm_rep (clshift c1) [seq clshift i | i <- cs]) +
size (rm_rep (crshift c1) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
k:'I_m
dE:d = k + n
(size cs).+1 =
size
(if clshift c == clshift c1
then rm_rep (clshift c1) [seq clshift i | i <- cs]
else
clshift c1
:: rm_rep (clshift c1) [seq clshift i | i <- cs]) +
size
(if crshift c == crshift c1
then rm_rep (crshift c1) [seq crshift i | i <- cs]
else
crshift c1
:: rm_rep (crshift c1) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
k:'I_m
dE:d = k + n
(size cs).+1 =
size
(if clshift c == clshift c1
then rm_rep (clshift c1) [seq clshift i | i <- cs]
else
clshift c1
:: rm_rep (clshift c1) [seq clshift i | i <- cs]) +
size
(if crshift c == crshift c1
then rm_rep (crshift c1) [seq crshift i | i <- cs]
else
crshift c1
:: rm_rep (crshift c1) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
k:'I_m
dE:d = k + n
clshift c != clshift c1
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
k:'I_m
dE:d = k + n
(size cs).+1 =
(size (rm_rep (clshift c1) [seq clshift i | i <- cs])).+1 +
size
(if crshift c == crshift c1
then rm_rep (crshift c1) [seq crshift i | i <- cs]
else
crshift c1
:: rm_rep (crshift c1) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
k:'I_m
dE:d = k + n
cE:c (tlshift n k) = c1 (tlshift n k)
False
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
k:'I_m
dE:d = k + n
(size cs).+1 =
(size (rm_rep (clshift c1) [seq clshift i | i <- cs])).+1 +
size
(if crshift c == crshift c1
then rm_rep (crshift c1) [seq crshift i | i <- cs]
else
crshift c1
:: rm_rep (crshift c1) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
k:'I_m
dE:d = k + n
cE:c (tlshift n k) = c1 (tlshift n k)
c d = c1 d
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
k:'I_m
dE:d = k + n
(size cs).+1 =
(size (rm_rep (clshift c1) [seq clshift i | i <- cs])).+1 +
size
(if crshift c == crshift c1
then rm_rep (crshift c1) [seq crshift i | i <- cs]
else
crshift c1
:: rm_rep (crshift c1) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
k:'I_m
dE:d = k + n
(size cs).+1 =
(size (rm_rep (clshift c1) [seq clshift i | i <- cs])).+1 +
size
(if crshift c == crshift c1
then rm_rep (crshift c1) [seq crshift i | i <- cs]
else
crshift c1
:: rm_rep (crshift c1) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
k:'I_m
dE:d = k + n
crshift c == crshift c1
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
k:'I_m
dE:d = k + n
(size cs).+1 =
(size (rm_rep (clshift c1) [seq clshift i | i <- cs])).+1 +
size (rm_rep (crshift c1) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
k:'I_m
dE:d = k + n
i:ordinal_finType n
c (trshift m i) = c1 (trshift m i)
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
k:'I_m
dE:d = k + n
(size cs).+1 =
(size (rm_rep (clshift c1) [seq clshift i | i <- cs])).+1 +
size (rm_rep (crshift c1) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
k:'I_m
dE:d = k + n
i:ordinal_finType n
d == i -> False
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
k:'I_m
dE:d = k + n
(size cs).+1 =
(size (rm_rep (clshift c1) [seq clshift i | i <- cs])).+1 +
size (rm_rep (crshift c1) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
k:'I_m
dE:d = k + n
(size cs).+1 =
(size (rm_rep (clshift c1) [seq clshift i | i <- cs])).+1 +
size (rm_rep (crshift c1) [seq crshift i | i <- cs])
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
c1:configuration (m + n)
cs:seq (configuration (m + n))
IH:forallc : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
c:configuration (m + n)
d:ordinal_finType (m + n)
d2H:r (c d) (c1 d)
d2H1:foralld2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2:on_top d c
d2H3:on_top d c1
c1Pcs:path move c1 cs
k:'I_m
dE:d = k + n
size cs =
(fix add (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| p.+1 => (add p m).+1end)
(size
(rm_rep (clshift c1) [seq clshift i | i <- cs]))
(size
(rm_rep (crshift c1) [seq crshift i | i <- cs]))
↓[c2] = last ↓[c1] (rm_rep ↓[c1] [seq ↓[i] | i <- p])
byrewrite last_rm_rep c2E last_map.Qed.
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
p:peg
cliftrn m p `c[p] = `c[p]
q:nat
r:rel peg
irH:irreflexive r
symH:symmetric r
m, n:nat
p:peg
cliftrn m p `c[p] = `c[p]
byapply/ffunP => i; rewrite !ffunE; case: tsplitP => j; rewrite !ffunE.Qed.(* case distinction that depends if the largest disk has move *)(* if it has not moved, we get the path on the unlifted configuration *)(* uf it has moved, we get the decomposition till the first move *)InductivepathS_spec (n : nat) (c : configuration n.+1)
(cs : seq (configuration n.+1)) :
forall (b : bool), Type
:=
pathS_specW :
forall (p := c ldisk) (c1 := ↓[c]) (cs1 := [seq ↓[i] | i <- cs]),
cs = [seq ↑[i]_p | i <- cs1] -> path move c1 cs1 -> pathS_spec c cs true |
pathS_spec_move :
forall (p1 := c ldisk) p2cs1cs2
(c1 := ↓[c])
(c2 := ↑[last c1 cs1]_p2),
p1 != p2 -> r p1 p2 ->
cs = [seq ↑[i]_p1 | i <- cs1] ++ c2 :: cs2 ->
path move c1 cs1 -> move ↑[last c1 cs1]_p1 c2 ->
path move c2 cs2 ->
pathS_spec c cs true |
pathS_spec_false : pathS_spec c cs false.(* Inversion theorem on a path for disk n.+1 *)
bycase: (p) H2 => [->//|c3 p1 _]; rewrite rev_cons last_rcons.Qed.EndGHanoi.Arguments perfect {q n}.Arguments cunliftr {q n}.Notation" ↑[ c ]_ p" := (cliftr p c) (at level5, format"↑[ c ]_ p").Notation" ↓[ c ]" := (cunliftr c) (at level5, format"↓[ c ]").Notation"`c[ p ] " := (perfect p) (format"`c[ p ]", at level5).Notation"`c[ p , n ] " := ((perfect p) : configuration _ n)
(format"`c[ p , n ]", at level5).
k:nat
d:disk 1
c:configuration k 1
on_top d c
k:nat
d:disk 1
c:configuration k 1
on_top d c
byapply/on_topP=> [] [] [] //=; case: d => [] [].Qed.
byrewrite eq_sym neq_bump.Qed.EndPLift.SectionCrlift.Variableq : nat.Variablep : peg q.+1.Variabler1 : rel (disk q).Variabler2 : rel (disk q.+1).Hypothesisr2Irr : irreflexive r2.Hypothesisr1Rr2 : forallij : disk q, r1 i j = r2 (lift p i) (lift p j).
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
move r2 (cliftln n p (plift p c1))
(cliftln n p (plift p c2)) = move r1 c1 c2
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
move r2 (cliftln n p (plift p c1))
(cliftln n p (plift p c2)) = move r1 c1 c2
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
H:move r1 c1 c2
move r2 (cliftln n p (plift p c1))
(cliftln n p (plift p c2))
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
H:move r2 (cliftln n p (plift p c1))
(cliftln n p (plift p c2))
move r1 c1 c2
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
H:move r1 c1 c2
cdisjoint (plift p c1) `c[p]
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
H:move r1 c1 c2
cdisjoint (plift p c2) `c[p]
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
H:move r1 c1 c2
move r2 (plift p c1) (plift p c2)
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
H:move r2 (cliftln n p (plift p c1))
(cliftln n p (plift p c2))
move r1 c1 c2
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
H:move r1 c1 c2
cdisjoint (plift p c1) `c[p]
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
H:move r1 c1 c2
cdisjoint (plift p c2) `c[p]
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
H:move r1 c1 c2
move r2 (plift p c1) (plift p c2)
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
H:move r2 (cliftln n p (plift p c1))
(cliftln n p (plift p c2))
move r1 c1 c2
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
H:move r1 c1 c2
cdisjoint (plift p c2) `c[p]
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
H:move r1 c1 c2
move r2 (plift p c1) (plift p c2)
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
H:move r2 (cliftln n p (plift p c1))
(cliftln n p (plift p c2))
move r1 c1 c2
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
H:move r1 c1 c2
cdisjoint (plift p c2) `c[p]
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
H:move r1 c1 c2
move r2 (plift p c1) (plift p c2)
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
H:move r2 (cliftln n p (plift p c1))
(cliftln n p (plift p c2))
move r1 c1 c2
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
H:move r1 c1 c2
move r2 (plift p c1) (plift p c2)
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
H:move r2 (cliftln n p (plift p c1))
(cliftln n p (plift p c2))
move r1 c1 c2
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
H:move r2 (cliftln n p (plift p c1))
(cliftln n p (plift p c2))
move r1 c1 c2
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
H:move r2 (cliftln n p (plift p c1))
(cliftln n p (plift p c2))
move r2 (plift p c1) (plift p c2) -> move r1 c1 c2
byrewrite (@plift_move _ _ _ r1).Qed.
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c:configuration q m
cs:seq (configuration q m)
path (move r2) (cliftln n p (plift p c))
[seq (cliftln n p \o plift p) i | i <- cs] =
path (move r1) c cs
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c:configuration q m
cs:seq (configuration q m)
path (move r2) (cliftln n p (plift p c))
[seq (cliftln n p \o plift p) i | i <- cs] =
path (move r1) c cs
byelim: cs c => //= c1 cs1 IH c; rewrite move_liftln IH.Qed.
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
connect (move r1) c1 c2 ->
connect (move r2) (cliftln n p (plift p c1))
(cliftln n p (plift p c2))
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
connect (move r1) c1 c2 ->
connect (move r2) (cliftln n p (plift p c1))
(cliftln n p (plift p c2))
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
x:seq
(finfun_finType (ordinal_finType m)
(ordinal_finType q))
Hp:path (move r2) (cliftln n p (plift p c1))
[seq (cliftln n p \o plift p) i | i <- x]
Hl:c2 = last c1 x
connect (move r2) (cliftln n p (plift p c1))
(cliftln n p (plift p c2))
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
x:seq
(finfun_finType (ordinal_finType m)
(ordinal_finType q))
Hp:path (move r2) (cliftln n p (plift p c1))
[seq (cliftln n p \o plift p) i | i <- x]
Hl:c2 = last c1 x
cliftln n p (plift p c2) =
last (cliftln n p (plift p c1))
[seq (cliftln n p \o plift p) i | i <- x]
byrewrite Hl [RHS]last_map.Qed.
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
connect (move r1) c1 c2 ->
`d[cliftln n p (plift p c1), cliftln n p (plift p c2)]_
(move r2) <= `d[c1, c2]_(move r1)
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
connect (move r1) c1 c2 ->
`d[cliftln n p (plift p c1), cliftln n p (plift p c2)]_
(move r2) <= `d[c1, c2]_(move r1)
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
p1:seq
(finfun_finType (ordinal_finType m)
(ordinal_finType q))
p1H:gpath (move r1) c1 c2 p1
`d[cliftln n p (plift p c1), cliftln n p (plift p c2)]_
(move r2) <= `d[c1, c2]_(move r1)
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
p1:seq
(finfun_finType (ordinal_finType m)
(ordinal_finType q))
p1H:gpath (move r1) c1 c2 p1
`d[cliftln n p (plift p c1), cliftln n p (plift p c2)]_
(move r2) <=
size [seq (cliftln n p \o plift p) i | i <- p1]
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
m, n:nat
c1, c2:configuration q m
p1:seq
(finfun_finType (ordinal_finType m)
(ordinal_finType q))
p1H:gpath (move r1) c1 c2 p1
last (cliftln n p (plift p c1))
[seq (cliftln n p \o plift p) i | i <- p1] =
cliftln n p (plift p c2)
byrewrite [LHS]last_map (gpath_last p1H).Qed.
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
n, m:nat
p1:peg q.+1
cliftln n p `c[p1] = cliftrn m p1 `c[p]
q:nat
p:peg q.+1
r1:rel (disk q)
r2:rel (disk q.+1)
r2Irr:irreflexive r2
r1Rr2:forallij : disk q,
r1 i j = r2 (lift p i) (lift p j)
n, m:nat
p1:peg q.+1
cliftln n p `c[p1] = cliftrn m p1 `c[p]
by [].Qed.EndCrlift.(******************************************************************************)(* Other peg *)(******************************************************************************)Definitionopegn (p1p2 : peg n) :=
odflt (if p1 <= p2 then p1 else p2) [pick i | (i != p1) && (i != p2)].
n:nat
p1, p2:peg n
opeg p1 p2 = opeg p2 p1
n:nat
p1, p2:peg n
opeg p1 p2 = opeg p2 p1
n:nat
p1, p2:peg n
H:p1 = p2
odflt p1 [pick i | i != p1 & i != p2] =
odflt p2 [pick i | i != p2 & i != p1]
n:nat
p1, p2:peg n
H:p1 = p2
p1 = p2
byapply/val_eqP/eqP.Qed.
n:nat
p1, p2:peg n.+3
opeg p1 p2 != p1
n:nat
p1, p2:peg n.+3
opeg p1 p2 != p1
n:nat
p1, p2:peg n.+3
HD:(funi : ordinal_finType n.+3 =>
(i != p1) && (i != p2)) =1 xpred0
odflt (if p1 <= p2 then p1 else p2) None != p1
n:nat
p1, p2:peg n.+3
HD:(funi : ordinal_finType n.+3 =>
(i != p1) && (i != p2)) =1 xpred0
p3, p4:peg n.+3
(p3 == p4) = (val p3 == val p4)
n:nat
p1, p2:peg n.+3
HD:(funi : ordinal_finType n.+3 =>
(i != p1) && (i != p2)) =1 xpred0
byapply: IH.Qed.Definitionsorted (s : seq nat) :=
forallij, i < size s -> j < size s -> (nth 0 s i < nth 0 s j) = (i < j).
a:nat
s:seq nat
sorted (a :: s) -> sorted s
a:nat
s:seq nat
sorted (a :: s) -> sorted s
bymove=> H i j iH jH; rewrite -[in RHS]ltnS -[in RHS]H.Qed.
i, j:nat
sorted (iota i j)
i, j:nat
sorted (iota i j)
i, j, i1, j1:nat
i1Lj:i1 < j
j1Lj:j1 < j
(nth 0 (iota i j) i1 < nth 0 (iota i j) j1) =
(i1 < j1)
byrewrite !nth_iota // ltn_add2l.Qed.
a, b:nat
s:seq nat
sorted [:: a, b & s] -> sorted (a :: s)
a, b:nat
s:seq nat
sorted [:: a, b & s] -> sorted (a :: s)
a, b:nat
s:seq nat
Hs:sorted [:: a, b & s]
j:nat
iH:0 < size (a :: s)
jH:j.+1 < size (a :: s)
(a < nth 0 s j) = (0 < j.+1)
a, b:nat
s:seq nat
Hs:sorted [:: a, b & s]
i:nat
iH:i.+1 < size (a :: s)
jH:0 < size (a :: s)
(nth 0 s i < a) = (i.+1 < 0)
a, b:nat
s:seq nat
Hs:sorted [:: a, b & s]
i, j:nat
iH:i.+1 < size (a :: s)
jH:j.+1 < size (a :: s)
(nth 0 s i < nth 0 s j) = (i.+1 < j.+1)
a, b:nat
s:seq nat
Hs:sorted [:: a, b & s]
j:nat
iH:0 < size (a :: s)
jH:j.+1 < size (a :: s)
(a < nth 0 s j) = (0 < j.+1)
a, b:nat
s:seq nat
Hs:sorted [:: a, b & s]
i:nat
iH:i.+1 < size (a :: s)
jH:0 < size (a :: s)
(nth 0 s i < a) = (i.+1 < 0)
a, b:nat
s:seq nat
Hs:sorted [:: a, b & s]
i, j:nat
iH:i.+1 < size (a :: s)
jH:j.+1 < size (a :: s)
(nth 0 s i < nth 0 s j) = (i.+1 < j.+1)
a, b:nat
s:seq nat
Hs:sorted [:: a, b & s]
i:nat
iH:i.+1 < size (a :: s)
jH:0 < size (a :: s)
(nth 0 s i < a) = (i.+1 < 0)
a, b:nat
s:seq nat
Hs:sorted [:: a, b & s]
i, j:nat
iH:i.+1 < size (a :: s)
jH:j.+1 < size (a :: s)
(nth 0 s i < nth 0 s j) = (i.+1 < j.+1)
a, b:nat
s:seq nat
Hs:sorted [:: a, b & s]
i:nat
iH:i.+1 < size (a :: s)
jH:0 < size (a :: s)
(nth 0 s i < a) = (i.+1 < 0)
a, b:nat
s:seq nat
Hs:sorted [:: a, b & s]
i, j:nat
iH:i.+1 < size (a :: s)
jH:j.+1 < size (a :: s)
(nth 0 s i < nth 0 s j) = (i.+1 < j.+1)
a, b:nat
s:seq nat
Hs:sorted [:: a, b & s]
i, j:nat
iH:i.+1 < size (a :: s)
jH:j.+1 < size (a :: s)
(nth 0 s i < nth 0 s j) = (i.+1 < j.+1)
byrewrite (Hs i.+2 j.+2).Qed.
s:seq nat
p:pred nat
sorted s -> sorted [seq x <- s | p x]
s:seq nat
p:pred nat
sorted s -> sorted [seq x <- s | p x]
s:seq nat
p:pred nat
a:nat
s1:seq nat
i:nat
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
s:seq nat
p:pred nat
F:forall (a : nat) (s1 : seq nat) (i : nat),
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
sorted s -> sorted [seq x <- s | p x]
s:seq nat
p:pred nat
a, b:nat
s1:seq nat
IH:foralli : nat,
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
i:nat
abS:sorted [:: a, b & s1]
i <
size
(if p b
then b :: [seq x <- s1 | p x]
else [seq x <- s1 | p x]) ->
a <
nth 0
(if p b
then b :: [seq x <- s1 | p x]
else [seq x <- s1 | p x]) i
s:seq nat
p:pred nat
F:forall (a : nat) (s1 : seq nat) (i : nat),
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
sorted s -> sorted [seq x <- s | p x]
s:seq nat
p:pred nat
a, b:nat
s1:seq nat
IH:foralli : nat,
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
i:nat
abS:sorted [:: a, b & s1]
pbT:p b
i < size (b :: [seq x <- s1 | p x]) ->
a < nth 0 (b :: [seq x <- s1 | p x]) i
s:seq nat
p:pred nat
a, b:nat
s1:seq nat
IH:foralli : nat,
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
i:nat
abS:sorted [:: a, b & s1]
pbF:~~ p b
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
s:seq nat
p:pred nat
F:forall (a : nat) (s1 : seq nat) (i : nat),
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
sorted s -> sorted [seq x <- s | p x]
s:seq nat
p:pred nat
a, b:nat
s1:seq nat
IH:foralli : nat,
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
abS:sorted [:: a, b & s1]
pbT:p b
i1:nat
sH:i1.+1 < (size [seq x <- s1 | p x]).+1
a < nth 0 [seq x <- s1 | p x] i1
s:seq nat
p:pred nat
a, b:nat
s1:seq nat
IH:foralli : nat,
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
i:nat
abS:sorted [:: a, b & s1]
pbF:~~ p b
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
s:seq nat
p:pred nat
F:forall (a : nat) (s1 : seq nat) (i : nat),
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
sorted s -> sorted [seq x <- s | p x]
s:seq nat
p:pred nat
a, b:nat
s1:seq nat
abS:sorted [:: a, b & s1]
pbT:p b
i1:nat
sH:i1.+1 < (size [seq x <- s1 | p x]).+1
sorted (a :: s1)
s:seq nat
p:pred nat
a, b:nat
s1:seq nat
IH:foralli : nat,
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
i:nat
abS:sorted [:: a, b & s1]
pbF:~~ p b
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
s:seq nat
p:pred nat
F:forall (a : nat) (s1 : seq nat) (i : nat),
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
sorted s -> sorted [seq x <- s | p x]
s:seq nat
p:pred nat
a, b:nat
s1:seq nat
IH:foralli : nat,
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
i:nat
abS:sorted [:: a, b & s1]
pbF:~~ p b
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
s:seq nat
p:pred nat
F:forall (a : nat) (s1 : seq nat) (i : nat),
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
sorted s -> sorted [seq x <- s | p x]
s:seq nat
p:pred nat
a, b:nat
s1:seq nat
i:nat
abS:sorted [:: a, b & s1]
pbF:~~ p b
sorted (a :: s1)
s:seq nat
p:pred nat
F:forall (a : nat) (s1 : seq nat) (i : nat),
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
sorted s -> sorted [seq x <- s | p x]
s:seq nat
p:pred nat
F:forall (a : nat) (s1 : seq nat) (i : nat),
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
sorted s -> sorted [seq x <- s | p x]
p:pred nat
F:forall (a : nat) (s1 : seq nat) (i : nat),
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
a:nat
s:seq nat
IH:sorted s -> sorted [seq x <- s | p x]
aS:sorted (a :: s)
sorted
(if p a
then a :: [seq x <- s | p x]
else [seq x <- s | p x])
p:pred nat
F:forall (a : nat) (s1 : seq nat) (i : nat),
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
a:nat
s:seq nat
IH:sorted s -> sorted [seq x <- s | p x]
aS:sorted (a :: s)
sS:sorted s
sorted
(if p a
then a :: [seq x <- s | p x]
else [seq x <- s | p x])
p:pred nat
F:forall (a : nat) (s1 : seq nat) (i : nat),
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
a:nat
s:seq nat
IH:sorted s -> sorted [seq x <- s | p x]
aS:sorted (a :: s)
sS:sorted s
paT:p a
sorted (a :: [seq x <- s | p x])
p:pred nat
F:forall (a : nat) (s1 : seq nat) (i : nat),
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
a:nat
s:seq nat
IH:sorted s -> sorted [seq x <- s | p x]
aS:sorted (a :: s)
sS:sorted s
paT:p a
iH, jH:0 < size (a :: [seq x <- s | p x])
(a < a) = (0 < 0)
p:pred nat
F:forall (a : nat) (s1 : seq nat) (i : nat),
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
a:nat
s:seq nat
IH:sorted s -> sorted [seq x <- s | p x]
aS:sorted (a :: s)
sS:sorted s
paT:p a
j:nat
iH:0 < size (a :: [seq x <- s | p x])
jH:j.+1 < size (a :: [seq x <- s | p x])
(a < nth 0 [seq x <- s | p x] j) = (0 < j.+1)
p:pred nat
F:forall (a : nat) (s1 : seq nat) (i : nat),
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
a:nat
s:seq nat
IH:sorted s -> sorted [seq x <- s | p x]
aS:sorted (a :: s)
sS:sorted s
paT:p a
i:nat
iH:i.+1 < size (a :: [seq x <- s | p x])
jH:0 < size (a :: [seq x <- s | p x])
(nth 0 [seq x <- s | p x] i < a) = (i.+1 < 0)
p:pred nat
F:forall (a : nat) (s1 : seq nat) (i : nat),
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
a:nat
s:seq nat
IH:sorted s -> sorted [seq x <- s | p x]
aS:sorted (a :: s)
sS:sorted s
paT:p a
i, j:nat
iH:i.+1 < size (a :: [seq x <- s | p x])
jH:j.+1 < size (a :: [seq x <- s | p x])
(nth 0 [seq x <- s | p x] i <
nth 0 [seq x <- s | p x] j) = (i.+1 < j.+1)
p:pred nat
F:forall (a : nat) (s1 : seq nat) (i : nat),
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
a:nat
s:seq nat
IH:sorted s -> sorted [seq x <- s | p x]
aS:sorted (a :: s)
sS:sorted s
paT:p a
iH, jH:0 < size (a :: [seq x <- s | p x])
(a < a) = (0 < 0)
p:pred nat
F:forall (a : nat) (s1 : seq nat) (i : nat),
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
a:nat
s:seq nat
IH:sorted s -> sorted [seq x <- s | p x]
aS:sorted (a :: s)
sS:sorted s
paT:p a
j:nat
iH:0 < size (a :: [seq x <- s | p x])
jH:j.+1 < size (a :: [seq x <- s | p x])
(a < nth 0 [seq x <- s | p x] j) = (0 < j.+1)
p:pred nat
F:forall (a : nat) (s1 : seq nat) (i : nat),
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
a:nat
s:seq nat
IH:sorted s -> sorted [seq x <- s | p x]
aS:sorted (a :: s)
sS:sorted s
paT:p a
i:nat
iH:i.+1 < size (a :: [seq x <- s | p x])
jH:0 < size (a :: [seq x <- s | p x])
(nth 0 [seq x <- s | p x] i < a) = (i.+1 < 0)
p:pred nat
F:forall (a : nat) (s1 : seq nat) (i : nat),
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
a:nat
s:seq nat
IH:sorted s -> sorted [seq x <- s | p x]
aS:sorted (a :: s)
sS:sorted s
paT:p a
i, j:nat
iH:i.+1 < size (a :: [seq x <- s | p x])
jH:j.+1 < size (a :: [seq x <- s | p x])
(nth 0 [seq x <- s | p x] i <
nth 0 [seq x <- s | p x] j) = (i.+1 < j.+1)
p:pred nat
F:forall (a : nat) (s1 : seq nat) (i : nat),
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
a:nat
s:seq nat
IH:sorted s -> sorted [seq x <- s | p x]
aS:sorted (a :: s)
sS:sorted s
paT:p a
j:nat
iH:0 < size (a :: [seq x <- s | p x])
jH:j.+1 < size (a :: [seq x <- s | p x])
(a < nth 0 [seq x <- s | p x] j) = (0 < j.+1)
p:pred nat
F:forall (a : nat) (s1 : seq nat) (i : nat),
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
a:nat
s:seq nat
IH:sorted s -> sorted [seq x <- s | p x]
aS:sorted (a :: s)
sS:sorted s
paT:p a
i:nat
iH:i.+1 < size (a :: [seq x <- s | p x])
jH:0 < size (a :: [seq x <- s | p x])
(nth 0 [seq x <- s | p x] i < a) = (i.+1 < 0)
p:pred nat
F:forall (a : nat) (s1 : seq nat) (i : nat),
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
a:nat
s:seq nat
IH:sorted s -> sorted [seq x <- s | p x]
aS:sorted (a :: s)
sS:sorted s
paT:p a
i, j:nat
iH:i.+1 < size (a :: [seq x <- s | p x])
jH:j.+1 < size (a :: [seq x <- s | p x])
(nth 0 [seq x <- s | p x] i <
nth 0 [seq x <- s | p x] j) = (i.+1 < j.+1)
p:pred nat
F:forall (a : nat) (s1 : seq nat) (i : nat),
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
a:nat
s:seq nat
IH:sorted s -> sorted [seq x <- s | p x]
aS:sorted (a :: s)
sS:sorted s
paT:p a
j:nat
iH:0 < size (a :: [seq x <- s | p x])
jH:j.+1 < size (a :: [seq x <- s | p x])
(a < nth 0 [seq x <- s | p x] j) = (0 < j.+1)
p:pred nat
F:forall (a : nat) (s1 : seq nat) (i : nat),
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
a:nat
s:seq nat
IH:sorted s -> sorted [seq x <- s | p x]
aS:sorted (a :: s)
sS:sorted s
paT:p a
i:nat
iH:i.+1 < size (a :: [seq x <- s | p x])
jH:0 < size (a :: [seq x <- s | p x])
(nth 0 [seq x <- s | p x] i < a) = (i.+1 < 0)
p:pred nat
F:forall (a : nat) (s1 : seq nat) (i : nat),
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
a:nat
s:seq nat
IH:sorted s -> sorted [seq x <- s | p x]
aS:sorted (a :: s)
sS:sorted s
paT:p a
i, j:nat
iH:i.+1 < size (a :: [seq x <- s | p x])
jH:j.+1 < size (a :: [seq x <- s | p x])
(nth 0 [seq x <- s | p x] i <
nth 0 [seq x <- s | p x] j) = (i.+1 < j.+1)
p:pred nat
F:forall (a : nat) (s1 : seq nat) (i : nat),
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
a:nat
s:seq nat
IH:sorted s -> sorted [seq x <- s | p x]
aS:sorted (a :: s)
sS:sorted s
paT:p a
i:nat
iH:i.+1 < size (a :: [seq x <- s | p x])
jH:0 < size (a :: [seq x <- s | p x])
(nth 0 [seq x <- s | p x] i < a) = (i.+1 < 0)
p:pred nat
F:forall (a : nat) (s1 : seq nat) (i : nat),
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
a:nat
s:seq nat
IH:sorted s -> sorted [seq x <- s | p x]
aS:sorted (a :: s)
sS:sorted s
paT:p a
i, j:nat
iH:i.+1 < size (a :: [seq x <- s | p x])
jH:j.+1 < size (a :: [seq x <- s | p x])
(nth 0 [seq x <- s | p x] i <
nth 0 [seq x <- s | p x] j) = (i.+1 < j.+1)
p:pred nat
F:forall (a : nat) (s1 : seq nat) (i : nat),
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
a:nat
s:seq nat
IH:sorted s -> sorted [seq x <- s | p x]
aS:sorted (a :: s)
sS:sorted s
paT:p a
i:nat
iH:i.+1 < size (a :: [seq x <- s | p x])
jH:0 < size (a :: [seq x <- s | p x])
(nth 0 [seq x <- s | p x] i < a) = (i.+1 < 0)
p:pred nat
F:forall (a : nat) (s1 : seq nat) (i : nat),
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
a:nat
s:seq nat
IH:sorted s -> sorted [seq x <- s | p x]
aS:sorted (a :: s)
sS:sorted s
paT:p a
i, j:nat
iH:i.+1 < size (a :: [seq x <- s | p x])
jH:j.+1 < size (a :: [seq x <- s | p x])
(nth 0 [seq x <- s | p x] i <
nth 0 [seq x <- s | p x] j) = (i.+1 < j.+1)
p:pred nat
F:forall (a : nat) (s1 : seq nat) (i : nat),
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
a:nat
s:seq nat
IH:sorted s -> sorted [seq x <- s | p x]
aS:sorted (a :: s)
sS:sorted s
paT:p a
i, j:nat
iH:i.+1 < size (a :: [seq x <- s | p x])
jH:j.+1 < size (a :: [seq x <- s | p x])
(nth 0 [seq x <- s | p x] i <
nth 0 [seq x <- s | p x] j) = (i.+1 < j.+1)
byrewrite ltnS (IH sS).Qed.
m:nat
enum 'I_m.+1 = [seq inord i | i <- iota 0 m.+1]
m:nat
enum 'I_m.+1 = [seq inord i | i <- iota 0 m.+1]
m:nat
enum 'I_m.+1 =
[seq ([eta inord] \o nat_of_ord (n:=m.+1)) i
| i <- ord_enum m.+1]
m:nat
ord_enum m.+1 =
[seq ([eta inord] \o nat_of_ord (n:=m.+1)) i
| i <- ord_enum m.+1]
m:nat
a:'I_m.+1
l:seq 'I_m.+1
a :: l = inord a :: l
byrewrite inord_val.Qed.(* To be reworked ! *)
m:nat
s:{set 'I_m}
i, j:'I_#|s|
(enum_val i < enum_val j) = (i < j)
m:nat
s:{set 'I_m}
i, j:'I_#|s|
(enum_val i < enum_val j) = (i < j)
s:{set 'I_0}
forallij : 'I_#|s|,
(enum_val i < enum_val j) = (i < j)
m:nat
s:{set 'I_m.+1}
i, j:'I_#|s|
(enum_val i < enum_val j) = (i < j)
s:{set 'I_0}
forallij : 'I_#|set0|,
(enum_val i < enum_val j) = (i < j)
s:{set 'I_0}
s = set0
m:nat
s:{set 'I_m.+1}
i, j:'I_#|s|
(enum_val i < enum_val j) = (i < j)
s:{set 'I_0}
m:nat
H:m < #|set0|
j:'I_#|set0|
False
s:{set 'I_0}
s = set0
m:nat
s:{set 'I_m.+1}
i, j:'I_#|s|
(enum_val i < enum_val j) = (i < j)
s:{set 'I_0}
s = set0
m:nat
s:{set 'I_m.+1}
i, j:'I_#|s|
(enum_val i < enum_val j) = (i < j)
m:nat
s:{set 'I_m.+1}
i, j:'I_#|s|
(enum_val i < enum_val j) = (i < j)
m:nat
s:{set 'I_m.+1}
i, j:'I_#|s|
j < size (enum s) ->
i < size (enum s) ->
(enum_val i < enum_val j) = (i < j)
m:nat
s:{set 'I_m.+1}
i, j:'I_#|s|
iL:j <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
jL:i <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
(nth (enum_default i)
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x] i <
nth (enum_default j)
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x] j) = (i < j)
m:nat
s:{set 'I_m.+1}
i, j:'I_#|s|
iL:j <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
jL:i <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
(nth 0
[seq i
| i <- [seq inord i | i <- iota 0 m.+1]
& mem s i] i <
nth (enum_default j)
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x] j) = (i < j)
m:nat
s:{set 'I_m.+1}
i, j:'I_#|s|
iL:j <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
jL:i <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
(nth 0
[seq i
| i <- [seq inord i | i <- iota 0 m.+1]
& mem s i] i <
nth 0
[seq i
| i <- [seq inord i | i <- iota 0 m.+1]
& mem s i] j) = (i < j)
m:nat
s:{set 'I_m.+1}
i, j:'I_#|s|
iL:j <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
jL:i <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
k1, k2:nat
k1 + k2 <= m.+1 ->
[seq i
| i <- [seq inord i0 | i0 <- iota k1 k2]
& mem s i] =
[seq i0 <- iota k1 k2 | mem s (inord i0)]
m:nat
s:{set 'I_m.+1}
i, j:'I_#|s|
iL:j <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
jL:i <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
F:forallk1k2 : nat,
k1 + k2 <= m.+1 ->
[seq i
| i <- [seq inord i0 | i0 <- iota k1 k2]
& mem s i] =
[seq i0 <- iota k1 k2 | mem s (inord i0)]
(nth 0
[seq i
| i <- [seq inord i | i <- iota 0 m.+1]
& mem s i] i <
nth 0
[seq i
| i <- [seq inord i | i <- iota 0 m.+1]
& mem s i] j) = (i < j)
m:nat
s:{set 'I_m.+1}
i, j:'I_#|s|
iL:j <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
jL:i <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
[seq i
| i <- [seq inord i0 | i0 <- iota k1.+1 k2]
& i \in s] =
[seq i0 <- iota k1.+1 k2 | inord i0 \in s]
m:nat
s:{set 'I_m.+1}
i, j:'I_#|s|
iL:j <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
jL:i <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
F:forallk1k2 : nat,
k1 + k2 <= m.+1 ->
[seq i
| i <- [seq inord i0 | i0 <- iota k1 k2]
& mem s i] =
[seq i0 <- iota k1 k2 | mem s (inord i0)]
(nth 0
[seq i
| i <- [seq inord i | i <- iota 0 m.+1]
& mem s i] i <
nth 0
[seq i
| i <- [seq inord i | i <- iota 0 m.+1]
& mem s i] j) = (i < j)
m:nat
s:{set 'I_m.+1}
i, j:'I_#|s|
iL:j <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
jL:i <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
k2, k1:nat
k1k2Lm:k1 + k2.+1 <= m.+1
k1.+1 + k2 <= m.+1
m:nat
s:{set 'I_m.+1}
i, j:'I_#|s|
iL:j <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
jL:i <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
F:forallk1k2 : nat,
k1 + k2 <= m.+1 ->
[seq i
| i <- [seq inord i0 | i0 <- iota k1 k2]
& mem s i] =
[seq i0 <- iota k1 k2 | mem s (inord i0)]
(nth 0
[seq i
| i <- [seq inord i | i <- iota 0 m.+1]
& mem s i] i <
nth 0
[seq i
| i <- [seq inord i | i <- iota 0 m.+1]
& mem s i] j) = (i < j)
m:nat
s:{set 'I_m.+1}
i, j:'I_#|s|
iL:j <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
jL:i <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
F:forallk1k2 : nat,
k1 + k2 <= m.+1 ->
[seq i
| i <- [seq inord i0 | i0 <- iota k1 k2]
& mem s i] =
[seq i0 <- iota k1 k2 | mem s (inord i0)]
(nth 0
[seq i
| i <- [seq inord i | i <- iota 0 m.+1]
& mem s i] i <
nth 0
[seq i
| i <- [seq inord i | i <- iota 0 m.+1]
& mem s i] j) = (i < j)
m:nat
s:{set 'I_m.+1}
i, j:'I_#|s|
iL:j <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
jL:i <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
F:forallk1k2 : nat,
k1 + k2 <= m.+1 ->
[seq i
| i <- [seq inord i0 | i0 <- iota k1 k2]
& mem s i] =
[seq i0 <- iota k1 k2 | mem s (inord i0)]
(nth 0 [seq i0 <- iota 0 m.+1 | mem s (inord i0)] i <
nth 0 [seq i0 <- iota 0 m.+1 | mem s (inord i0)] j) =
(i < j)
m:nat
s:{set 'I_m.+1}
i, j:'I_#|s|
iL:j <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
jL:i <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
F:forallk1k2 : nat,
k1 + k2 <= m.+1 ->
[seq i
| i <- [seq inord i0 | i0 <- iota k1 k2]
& mem s i] =
[seq i0 <- iota k1 k2 | mem s (inord i0)]
j < size [seq i0 <- iota 0 m.+1 | mem s (inord i0)]
m:nat
s:{set 'I_m.+1}
i, j:'I_#|s|
iL:j <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
jL:i <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
F:forallk1k2 : nat,
k1 + k2 <= m.+1 ->
[seq i
| i <- [seq inord i0 | i0 <- iota k1 k2]
& mem s i] =
[seq i0 <- iota k1 k2 | mem s (inord i0)]
j < size [seq i0 <- iota 0 m.+1 | mem s (inord i0)] ->
(nth 0 [seq i0 <- iota 0 m.+1 | mem s (inord i0)] i <
nth 0 [seq i0 <- iota 0 m.+1 | mem s (inord i0)] j) =
(i < j)
m:nat
s:{set 'I_m.+1}
i, j:'I_#|s|
iL:j <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
jL:i <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
F:forallk1k2 : nat,
k1 + k2 <= m.+1 ->
[seq i
| i <- [seq inord i0 | i0 <- iota k1 k2]
& mem s i] =
[seq i0 <- iota k1 k2 | mem s (inord i0)]
j < size [seq i0 <- iota 0 m.+1 | mem s (inord i0)] ->
(nth 0 [seq i0 <- iota 0 m.+1 | mem s (inord i0)] i <
nth 0 [seq i0 <- iota 0 m.+1 | mem s (inord i0)] j) =
(i < j)
m:nat
s:{set 'I_m.+1}
i, j:'I_#|s|
iL:j <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
jL:i <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
F:forallk1k2 : nat,
k1 + k2 <= m.+1 ->
[seq i
| i <- [seq inord i0 | i0 <- iota k1 k2]
& mem s i] =
[seq i0 <- iota k1 k2 | mem s (inord i0)]
i < size [seq i0 <- iota 0 m.+1 | mem s (inord i0)] ->
j < size [seq i0 <- iota 0 m.+1 | mem s (inord i0)] ->
(nth 0 [seq i0 <- iota 0 m.+1 | mem s (inord i0)] i <
nth 0 [seq i0 <- iota 0 m.+1 | mem s (inord i0)] j) =
(i < j)
m:nat
s:{set 'I_m.+1}
i, j:'I_#|s|
iL:j <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
jL:i <
size
[seq x <- [seq inord i | i <- iota 0 m.+1]
| mem s x]
F:forallk1k2 : nat,
k1 + k2 <= m.+1 ->
[seq i
| i <- [seq inord i0 | i0 <- iota k1 k2]
& mem s i] =
[seq i0 <- iota k1 k2 | mem s (inord i0)]
sorted (iota 0 m.+1)
byapply: sorted_iota.Qed.SectionISetd.(* Number of disks *)Variablen : nat.(* Subset of disks *)Variablesd : {set disk n}.(* Number of pegs *)Variablek : nat.(* relations on peg *)Variablerel : rel (peg k).Definitioncset (c : configuration k n) : configuration k #|sd| :=
[ffun i => c (enum_val i)].
n:nat
sd:{set disk n}
k:nat
rel:ssrbool.rel (peg k)
c:configuration k n
d:ordinal_finType n
dIsd:d \in sd
on_top d c -> on_top (enum_rank_in dIsd d) (cset c)
n:nat
sd:{set disk n}
k:nat
rel:ssrbool.rel (peg k)
c:configuration k n
d:ordinal_finType n
dIsd:d \in sd
on_top d c -> on_top (enum_rank_in dIsd d) (cset c)
n:nat
sd:{set disk n}
k:nat
rel:ssrbool.rel (peg k)
c:configuration k n
d:ordinal_finType n
dIsd:d \in sd
dO:foralld1 : ordinal_finType n,
c d = c d1 -> d <= d1
on_top (enum_rank_in dIsd d) (cset c)
n:nat
sd:{set disk n}
k:nat
rel:ssrbool.rel (peg k)
c:configuration k n
d:ordinal_finType n
dIsd:d \in sd
dO:foralld1 : ordinal_finType n,
c d = c d1 -> d <= d1
d1:'I_#|[eta sd]|
H:cset c (enum_rank_in dIsd d) = cset c d1
enum_rank_in dIsd d <= d1
n:nat
sd:{set disk n}
k:nat
rel:ssrbool.rel (peg k)
c:configuration k n
d:ordinal_finType n
dIsd:d \in sd
dO:foralld1 : ordinal_finType n,
c d = c d1 -> d <= d1
d1:'I_#|[eta sd]|
H:cset c (enum_rank_in dIsd d) = cset c d1
dDd1:enum_rank_in dIsd d != d1
enum_rank_in dIsd d < d1
n:nat
sd:{set disk n}
k:nat
rel:ssrbool.rel (peg k)
c:configuration k n
d:ordinal_finType n
dIsd:d \in sd
dO:foralld1 : ordinal_finType n,
c d = c d1 -> d <= d1
d1:'I_#|[eta sd]|
H:cset c (enum_rank_in dIsd d) = cset c d1
dDd1:enum_rank_in dIsd d != d1
enum_val d1 \in sd
n:nat
sd:{set disk n}
k:nat
rel:ssrbool.rel (peg k)
c:configuration k n
d:ordinal_finType n
dIsd:d \in sd
dO:foralld1 : ordinal_finType n,
c d = c d1 -> d <= d1
d1:'I_#|[eta sd]|
H:cset c (enum_rank_in dIsd d) = cset c d1
dDd1:enum_rank_in dIsd d != d1
d < enum_val d1
n:nat
sd:{set disk n}
k:nat
rel:ssrbool.rel (peg k)
c:configuration k n
d:ordinal_finType n
dIsd:d \in sd
dO:foralld1 : ordinal_finType n,
c d = c d1 -> d <= d1
d1:'I_#|[eta sd]|
H:cset c (enum_rank_in dIsd d) = cset c d1
dDd1:enum_rank_in dIsd d != d1
d < enum_val d1
n:nat
sd:{set disk n}
k:nat
rel:ssrbool.rel (peg k)
c:configuration k n
d:ordinal_finType n
dIsd:d \in sd
dO:foralld1 : ordinal_finType n,
c d = c d1 -> d <= d1
d1:'I_#|[eta sd]|
H:cset c (enum_rank_in dIsd d) = cset c d1
dDd1:enum_rank_in dIsd d != d1
(d != enum_val d1) && (d <= enum_val d1)
n:nat
sd:{set disk n}
k:nat
rel:ssrbool.rel (peg k)
c:configuration k n
d:ordinal_finType n
dIsd:d \in sd
dO:foralld1 : ordinal_finType n,
c d = c d1 -> d <= d1
d1:'I_#|[eta sd]|
H:cset c (enum_rank_in dIsd d) = cset c d1
dDd1:enum_rank_in dIsd d != d1
dEd1:d = enum_val d1
~~ true && (d <= enum_val d1)
n:nat
sd:{set disk n}
k:nat
rel:ssrbool.rel (peg k)
c:configuration k n
d:ordinal_finType n
dIsd:d \in sd
dO:foralld1 : ordinal_finType n,
c d = c d1 -> d <= d1
d1:'I_#|[eta sd]|
H:cset c (enum_rank_in dIsd d) = cset c d1
dDd1:enum_rank_in dIsd d != d1
dDd1':d != enum_val d1
d <= enum_val d1
n:nat
sd:{set disk n}
k:nat
rel:ssrbool.rel (peg k)
c:configuration k n
d:ordinal_finType n
dIsd:d \in sd
dO:foralld1 : ordinal_finType n,
c d = c d1 -> d <= d1
d1:'I_#|[eta sd]|
H:cset c (enum_rank_in dIsd d) = cset c d1
dDd1:enum_rank_in dIsd d != d1
dDd1':d != enum_val d1
d <= enum_val d1
n:nat
sd:{set disk n}
k:nat
rel:ssrbool.rel (peg k)
c:configuration k n
d:ordinal_finType n
dIsd:d \in sd
dO:foralld1 : ordinal_finType n,
c d = c d1 -> d <= d1
byapply: gpath_path gH.Qed.EndISetd.Arguments gpath [T].SectionCSet.(* Number of disks *)Variablen : nat.(* cut limit *)Variablet : nat.VariabletLn : t <= n.(* Number of pegs *)Variablek : nat.(* relations on peg *)Variablerel : rel (peg k).HypothesisirH : irreflexive rel.Definitionccut (c : configuration k n) : configuration k t :=
[ffun i => c (widen_ord tLn i)].
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c:configuration k n
cs:seq (configuration k n)
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n, d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
(size cs).+1 =
size
(if ccut c == ccut c1
then rm_rep (ccut c1) [seq ccut i | i <- cs]
else
ccut c1 :: rm_rep (ccut c1) [seq ccut i | i <- cs]) +
size
(if ctuc c == ctuc c1
then rm_rep (ctuc c1) [seq ctuc i | i <- cs]
else
ctuc c1 :: rm_rep (ctuc c1) [seq ctuc i | i <- cs])
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n, d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
c d != c1 d
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n,
d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
(size cs).+1 =
size
(if ccut c == ccut c1
then rm_rep (ccut c1) [seq ccut i | i <- cs]
else
ccut c1 :: rm_rep (ccut c1) [seq ccut i | i <- cs]) +
size
(if ctuc c == ctuc c1
then rm_rep (ctuc c1) [seq ctuc i | i <- cs]
else
ctuc c1 :: rm_rep (ctuc c1) [seq ctuc i | i <- cs])
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n, d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
(size cs).+1 =
size
(if ccut c == ccut c1
then rm_rep (ccut c1) [seq ccut i | i <- cs]
else
ccut c1 :: rm_rep (ccut c1) [seq ccut i | i <- cs]) +
size
(if ctuc c == ctuc c1
then rm_rep (ctuc c1) [seq ctuc i | i <- cs]
else
ctuc c1 :: rm_rep (ctuc c1) [seq ctuc i | i <- cs])
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n, d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
dLt:d < t
(size cs).+1 =
size
(if ccut c == ccut c1
then rm_rep (ccut c1) [seq ccut i | i <- cs]
else
ccut c1 :: rm_rep (ccut c1) [seq ccut i | i <- cs]) +
size
(if ctuc c == ctuc c1
then rm_rep (ctuc c1) [seq ctuc i | i <- cs]
else
ctuc c1 :: rm_rep (ctuc c1) [seq ctuc i | i <- cs])
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n,
d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
tLd:t <= d
(size cs).+1 =
size
(if ccut c == ccut c1
then rm_rep (ccut c1) [seq ccut i | i <- cs]
else
ccut c1 :: rm_rep (ccut c1) [seq ccut i | i <- cs]) +
size
(if ctuc c == ctuc c1
then rm_rep (ctuc c1) [seq ctuc i | i <- cs]
else
ctuc c1 :: rm_rep (ctuc c1) [seq ctuc i | i <- cs])
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n, d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
dLt:d < t
ccut c != ccut c1
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n,
d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
dLt:d < t
(size cs).+1 =
(size (rm_rep (ccut c1) [seq ccut i | i <- cs]) +
size
(if ctuc c == ctuc c1
then rm_rep (ctuc c1) [seq ctuc i | i <- cs]
else
ctuc c1
:: rm_rep (ctuc c1) [seq ctuc i | i <- cs])).+1
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n,
d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
tLd:t <= d
(size cs).+1 =
size
(if ccut c == ccut c1
then rm_rep (ccut c1) [seq ccut i | i <- cs]
else
ccut c1 :: rm_rep (ccut c1) [seq ccut i | i <- cs]) +
size
(if ctuc c == ctuc c1
then rm_rep (ctuc c1) [seq ctuc i | i <- cs]
else
ctuc c1 :: rm_rep (ctuc c1) [seq ctuc i | i <- cs])
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n, d != d2 -> c d2 = c1 d2
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n,
d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
dLt:d < t
(size cs).+1 =
(size (rm_rep (ccut c1) [seq ccut i | i <- cs]) +
size
(if ctuc c == ctuc c1
then rm_rep (ctuc c1) [seq ctuc i | i <- cs]
else
ctuc c1
:: rm_rep (ctuc c1) [seq ctuc i | i <- cs])).+1
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n,
d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
tLd:t <= d
(size cs).+1 =
size
(if ccut c == ccut c1
then rm_rep (ccut c1) [seq ccut i | i <- cs]
else
ccut c1 :: rm_rep (ccut c1) [seq ccut i | i <- cs]) +
size
(if ctuc c == ctuc c1
then rm_rep (ctuc c1) [seq ctuc i | i <- cs]
else
ctuc c1 :: rm_rep (ctuc c1) [seq ctuc i | i <- cs])
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n, d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
dLt:d < t
(size cs).+1 =
(size (rm_rep (ccut c1) [seq ccut i | i <- cs]) +
size
(if ctuc c == ctuc c1
then rm_rep (ctuc c1) [seq ctuc i | i <- cs]
else
ctuc c1
:: rm_rep (ctuc c1) [seq ctuc i | i <- cs])).+1
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n,
d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
tLd:t <= d
(size cs).+1 =
size
(if ccut c == ccut c1
then rm_rep (ccut c1) [seq ccut i | i <- cs]
else
ccut c1 :: rm_rep (ccut c1) [seq ccut i | i <- cs]) +
size
(if ctuc c == ctuc c1
then rm_rep (ctuc c1) [seq ctuc i | i <- cs]
else
ctuc c1 :: rm_rep (ctuc c1) [seq ctuc i | i <- cs])
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n, d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
dLt:d < t
ctuc c == ctuc c1
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n,
d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
dLt:d < t
(size cs).+1 =
(size (rm_rep (ccut c1) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c1) [seq ctuc i | i <- cs])).+1
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n,
d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
tLd:t <= d
(size cs).+1 =
size
(if ccut c == ccut c1
then rm_rep (ccut c1) [seq ccut i | i <- cs]
else
ccut c1 :: rm_rep (ccut c1) [seq ccut i | i <- cs]) +
size
(if ctuc c == ctuc c1
then rm_rep (ctuc c1) [seq ctuc i | i <- cs]
else
ctuc c1 :: rm_rep (ctuc c1) [seq ctuc i | i <- cs])
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n, d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
dLt:d < t
i:ordinal_finType (n - t)
d != tuc_ord i
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n,
d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
dLt:d < t
(size cs).+1 =
(size (rm_rep (ccut c1) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c1) [seq ctuc i | i <- cs])).+1
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n,
d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
tLd:t <= d
(size cs).+1 =
size
(if ccut c == ccut c1
then rm_rep (ccut c1) [seq ccut i | i <- cs]
else
ccut c1 :: rm_rep (ccut c1) [seq ccut i | i <- cs]) +
size
(if ctuc c == ctuc c1
then rm_rep (ctuc c1) [seq ctuc i | i <- cs]
else
ctuc c1 :: rm_rep (ctuc c1) [seq ctuc i | i <- cs])
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n, d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
dLt:d < t
i:ordinal_finType (n - t)
val d == val (tuc_ord i) -> False
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n,
d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
dLt:d < t
(size cs).+1 =
(size (rm_rep (ccut c1) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c1) [seq ctuc i | i <- cs])).+1
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n,
d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
tLd:t <= d
(size cs).+1 =
size
(if ccut c == ccut c1
then rm_rep (ccut c1) [seq ccut i | i <- cs]
else
ccut c1 :: rm_rep (ccut c1) [seq ccut i | i <- cs]) +
size
(if ctuc c == ctuc c1
then rm_rep (ctuc c1) [seq ctuc i | i <- cs]
else
ctuc c1 :: rm_rep (ctuc c1) [seq ctuc i | i <- cs])
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n, d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
dLt:d < t
(size cs).+1 =
(size (rm_rep (ccut c1) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c1) [seq ctuc i | i <- cs])).+1
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n,
d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
tLd:t <= d
(size cs).+1 =
size
(if ccut c == ccut c1
then rm_rep (ccut c1) [seq ccut i | i <- cs]
else
ccut c1 :: rm_rep (ccut c1) [seq ccut i | i <- cs]) +
size
(if ctuc c == ctuc c1
then rm_rep (ctuc c1) [seq ctuc i | i <- cs]
else
ctuc c1 :: rm_rep (ctuc c1) [seq ctuc i | i <- cs])
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n, d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
tLd:t <= d
(size cs).+1 =
size
(if ccut c == ccut c1
then rm_rep (ccut c1) [seq ccut i | i <- cs]
else
ccut c1 :: rm_rep (ccut c1) [seq ccut i | i <- cs]) +
size
(if ctuc c == ctuc c1
then rm_rep (ctuc c1) [seq ctuc i | i <- cs]
else
ctuc c1 :: rm_rep (ctuc c1) [seq ctuc i | i <- cs])
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n, d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
tLd:t <= d
ccut c == ccut c1
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n,
d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
tLd:t <= d
(size cs).+1 =
size (rm_rep (ccut c1) [seq ccut i | i <- cs]) +
size
(if ctuc c == ctuc c1
then rm_rep (ctuc c1) [seq ctuc i | i <- cs]
else
ctuc c1 :: rm_rep (ctuc c1) [seq ctuc i | i <- cs])
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n, d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
tLd:t <= d
i:ordinal_finType t
d != widen_ord tLn i
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n,
d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
tLd:t <= d
(size cs).+1 =
size (rm_rep (ccut c1) [seq ccut i | i <- cs]) +
size
(if ctuc c == ctuc c1
then rm_rep (ctuc c1) [seq ctuc i | i <- cs]
else
ctuc c1 :: rm_rep (ctuc c1) [seq ctuc i | i <- cs])
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n, d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
tLd:t <= d
(size cs).+1 =
size (rm_rep (ccut c1) [seq ccut i | i <- cs]) +
size
(if ctuc c == ctuc c1
then rm_rep (ctuc c1) [seq ctuc i | i <- cs]
else
ctuc c1 :: rm_rep (ctuc c1) [seq ctuc i | i <- cs])
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n, d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
tLd:t <= d
ctuc c != ctuc c1
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n,
d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
tLd:t <= d
(size cs).+1 =
size (rm_rep (ccut c1) [seq ccut i | i <- cs]) +
(size (rm_rep (ctuc c1) [seq ctuc i | i <- cs])).+1
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n, d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
tLd:t <= d
ctuc c (otuc tLd) == ctuc c1 (otuc tLd) -> False
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n,
d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
tLd:t <= d
(size cs).+1 =
size (rm_rep (ccut c1) [seq ccut i | i <- cs]) +
(size (rm_rep (ctuc c1) [seq ctuc i | i <- cs])).+1
n, t:nat
tLn:t <= n
k:nat
rel:ssrbool.rel (peg k)
irH:irreflexive rel
c1:configuration k n
cs:seq (configuration k n)
IH:forallc : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c:configuration k n
d:ordinal_finType n
dH1:rel (c d) (c1 d)
dH2:foralld2 : ordinal_finType n, d != d2 -> c d2 = c1 d2
dH3:on_top d c
dH4:on_top d c1
c1Pcs:path (move rel) c1 cs
cdDc1d:c d != c1 d
tLd:t <= d
(size cs).+1 =
size (rm_rep (ccut c1) [seq ccut i | i <- cs]) +
(size (rm_rep (ctuc c1) [seq ctuc i | i <- cs])).+1
IH:forallc : configuration k n,
cvalid c && all cvalid cs ->
path (move rel1) c cs ->
path (move rel2) (cset2 c)
(rm_rep (cset2 c) [seq cset2 i | i <- cs])
c:configuration k n
c1V:cvalid c
c2V:cvalid c1
c3V:all cvalid cs
cMc1:move rel1 c c1
c1Pcs:path (move rel1) c1 cs
path (move rel2) (cset2 c)
(if cset2 c == cset2 c1
then rm_rep (cset2 c1) [seq cset2 i | i <- cs]
else
cset2 c1
:: rm_rep (cset2 c1) [seq cset2 i | i <- cs])
IH:forallc : configuration k n,
cvalid c && all cvalid cs ->
path (move rel1) c cs ->
path (move rel2) (cset2 c)
(rm_rep (cset2 c) [seq cset2 i | i <- cs])
c:configuration k n
c1V:cvalid c
c2V:cvalid c1
c3V:all cvalid cs
cMc1:move rel1 c c1
c1Pcs:path (move rel1) c1 cs
cDc1:cset2 c != cset2 c1
move rel2 (cset2 c) (cset2 c1) &&
path (move rel2) (cset2 c1)
(rm_rep (cset2 c1) [seq cset2 i | i <- cs])
IH:forallc : configuration k n,
cvalid c && all cvalid cs ->
path (move rel1) c cs ->
path (move rel2) (cset2 c)
(rm_rep (cset2 c) [seq cset2 i | i <- cs])